A:Type, l:IdLnk, tg:Id, ds:x:Id fp Type, conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
(k:Knd. (k  fpf-domain(conds))  (hasloc(k;source(l))))
 (i:Id. (R-has-loc(triggersGlue(A; l; tg; ds; conds);i))  (i = source(l))) 

latex

Definitions

x:A. B(x), Knd, Top, P  Q, t  T, x. t(x), , P  Q, b, ff, P  Q, P & Q, P  Q, if b then t else f fi , (x  l), x:A. B(x), A c B, A  B, A, False, triggersGlue(A; l; tg; ds; conds), x(s), reduce(f;k;as), Y, R-has-loc(R;i), trigger-send(A;ds;x;cond;l;tg), (xL.P(x)), , fpf-domain(f)

Lemmas

fpf-domain wf, fpf-trivial-subtype-top, decl-state wf, top wf, Rall wf, trigger-send wf, fpf-ap wf, member-fpf-dom, l member wf, Rlist-has-loc, assert wf, R-has-loc wf, triggersGlue wf, member-fpf-domain, fpf-dom wf, Knd wf, Kind-deq wf, Id wf, hasloc wf, lsrc wf, fpf wf, IdLnk wf, bor wf, Rsframe wf, bfalse wf, false wf, iff transitivity, assert of bor, or functionality wrt iff, assert-eq-id, assert-Rall-has-loc2, nat wf, length wf1, select wf